\begin{nusmvCommand} {bmc\_setup} {Builds the model in a Boolean Epression format.}

\cmdLine{bmc\_setup [-h]}

You must call this command before use any other bmc-related command.
Only one call per session is required.

\end{nusmvCommand}
